IrrelevantConstructor.agda:4,4-9
Irrelevant constructors are not supported
when checking the constructor c in the declaration of D
